\begin{dis}{\LARGE\scshape Darsena}
\especif
\\\hspace*{2em}Se usara el TAD Darsena($\alpha$)

\aspectos
\serviciosexp
\\ \hspace*{2em} Todas las operaciones se realizan por referencia\\
\orden{}{}
\orden{}{}
\orden{}{}
\orden{}{}
\orden{}{}
\orden{}{}
\orden{}{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\interfaz
\interface{Darsena(\alpha)}

\seexplica{Darsena(\alpha)}
\usa{\scshape Bool, Nat, \alpha, Conj, Cola \normalfont} 
\exporta{Darsena, estacionar, sacar, cantDarsenas, colaDarsena, aSalir, primerMicro, =$_{Darsena}$}
\genero{Darsena(\alpha)}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\operaciones

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{Darsena}{in n: Nat}{res: Darsena($\alpha$)}{}
   \precond{True}
   \poscond{\widehat{res} \igobs Nuevo(\widehat{n})}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{estacionar}{in a: $\alpha$, in n: Nat, inout d: Darsena($\alpha$)}{}
   \precond{True}
   \poscond{widehat{d} $\igobs$ estacionar(\widehat{a}, \widehat{n}, $d_0$}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{3em} \begin{funcion}{sacar}{in n: Nat, inout d: Darsena($\alpha$)}{}{}
   \precond{True}
   \poscond{\widehat{d} $\igobs$ sacar(\widehat{n}, $d_0$)}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{cantDarsenas}{in d: Darsena($\alpha$)}{res: Nat)}{}
   \precond{True}
   \poscond{widehat{res} $\igobs$ cantDarsenas(\widehat{d})}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{colaDarsena}{in n: Nat, in d: Darsena($\alpha$)}{res: Cola($\alpha$)}{}
   \precond{\whidehat{n} $\in$ aSalir(\widehat(d))}
   \poscond{widehat{res} $\igobs$ colaDarsena(\widehat{n}, \widehat{d})}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{aSalir}{in d: Darsena($\alpha$)}{res: Conj(Nat)}{}
   \precond{True}
   \poscond{\widehat{res} $\igobs$ aSalir(\widehat{d})}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{primerMicro}{in n: Nat, in d: Darsena($\alpha$)}{res: $\alpha$}{}
   \precond{\widehat{n} $\in$ aSalir(\widehat{d})}
   \poscond{widehat{res} $\igobs$ primerMicro(\widehat{n},$d_0$)}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{=$_{Darsena}$}{in d: Darsena($\alpha$), in p: Darsena($\alpha$)}{res: bool}{}
   \precond{True}
   \poscond{\widehat{res} \igobs d \igsub{Darsena} p} 
\end{funcion}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\pautas

\estructura \\ \normalfont
\\\hspace*{2em}Para cumplir los requerimientos pedidos, vamos a usar un arreglo Dimensionable con una
\\\hspace*{2em}secuencia en cada bucket y una funcion de hash para acomodar los elementos.

\\\hspace*{2em}Darsena se representa con \textbf{estrD}
\\\hspace*{2em}donde \textbf{estrD} es Tupla $<$ arD : arreglo$\_$dimensionable de Cola($\alpha$), cantD : Nat$>$ \\

\invariante\\
\\\hspace*{2em}Rep: \widehat{estrDicc} $\longrightarrow$ boolean \\
\\\hspace*{2em}($\forall$ e: estrDic) Rep(e) $\equiv$ ($\forall$ a: $\alpha$ $\in$ e.clavD)\\
\\\hspace*{2em} (
\funcabs \\
\\\hspace*{2em}Abs: \widehat{estrD} e $\longrightarrow$ Darsena \\\hspace*{4em}Res(e)\\
\\\hspace*{2em}($\forall$ e: \widehat{estrD}) Abs(e) $\equiv$ d: Darsena \\
\\\hspace*{2em} cantDarsenas(d) \igobs e.cantD \\
\\\hspace*{2em}($\forall$ a < cantDarsenas(d))
\\\hspace*{2em} colaDarsena(a, d) \igobs e.ard[a] \\

\end{dis}